/*
 * DNFTree.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef DNFTREE_HPP_
#define DNFTREE_HPP_

#include <utility>
#include <list>
#include <vector>

#include "bfr/Literal.hpp"
#include "bfr/ClauseSet.hpp"

namespace bfr {
// TODO remove final
// i think it is better to check if size() == 0...

/**
 * This class represents a <i>DNF Tree</i>.
 *
 * The DNF tree is created by the linear programming algorithm to
 * convert DNFs to LPBs.
 *
 * The tree consists of nodes that have a DNF as label.
 * Each Node has two child nodes, so it is a binary tree.
 */
class DNFTree {
    public:
        typedef std::list<std::list<Literal>* > content_t;
        DNFTree();
        ~DNFTree();

        static const size_t npos;
        size_t createRoot(const content_t *dnf, bool isFinal);
        size_t createLeftChild(size_t nodeID, const content_t *dnf,
                               bool isFinal);
        size_t createRightChild(size_t nodeID, const content_t *dnf,
                                bool isFinal);
        inline const content_t *getDNFEntry(size_t nodeID) const;
        inline bool getFinal(size_t nodeID) const;
        inline size_t getDepth(size_t nodeID) const;
        inline size_t size() const;
        inline size_t getLeftChild(size_t nodeID) const;
        inline size_t getRightChild(size_t nodeID) const;
        inline bool isLeaf(size_t nodeID) const;
        void deleteEntry(size_t nodeID);

    private:

        struct NodeContent {
            public:
                NodeContent(const content_t *dn, size_t lc, size_t rc,
                        bool f, size_t d)
                    : dnf(dn), leftChild(lc), rightChild(rc),
                      final(f), depth(d) { }
                const content_t *dnf;
                size_t leftChild;
                size_t rightChild;
                bool final;
                size_t depth;
        };

        size_t createNodeEntry(const content_t *dnf, size_t depth, bool isFinal);
        NodeContent &getNode(size_t id);

        //typedef std::pair<const content_t*, size_t> entry_t;
        // saves for each node the DNF and the position of the first
        // child node.
        //std::vector< entry_t > nodes;
        // saves for each node in nodes exactly two children
        // the node knows the position in this array
        //std::vector<size_t> children;
        // stores for each entry if it is final
        //std::vector<bool> final;
        // stores for each node its depth
        //std::vector<size_t> depths;

        std::vector<NodeContent> content;
};

// some inline methods

bool DNFTree::getFinal(size_t nodeID) const {
    //return final[nodeID];
    return content[nodeID].final;
}

size_t DNFTree::getDepth(size_t nodeID) const {
    //return depths[nodeID];
    return content[nodeID].depth;
}

size_t DNFTree::size() const {
    //return nodes.size();
    return content.size();
}

const DNFTree::content_t* DNFTree::getDNFEntry(size_t nodeID) const {
    //return nodes[nodeID].first;
    return content[nodeID].dnf;
}


size_t DNFTree::getLeftChild(size_t nodeID) const {
    //size_t firstChildPos = nodes[nodeID].second;
    //return children[firstChildPos];
    return content[nodeID].leftChild;
}

size_t DNFTree::getRightChild(size_t nodeID) const {
    //size_t firstChildPos = nodes[nodeID].second;
    //return children[firstChildPos + 1];
    return content[nodeID].rightChild;
}

bool DNFTree::isLeaf(size_t nodeID) const {
    /*size_t firstChildPos = nodes[nodeID].second;
    return ( (children[firstChildPos] == DNFTree::npos) &&
            (children[firstChildPos + 1] == DNFTree::npos));*/
    const NodeContent &n = content[nodeID];
    return (n.leftChild == DNFTree::npos) &&
           (n.rightChild == DNFTree::npos);
}

} // namespace bfr


#endif  // DNFTREE_HPP_
